Belnap の四値論理
データベースから推論を行ふ能力を備へた高度な質問應答システムを構築する場合、特定の四値論理を採用すべきであるとの主張がある。その根據となるのは、データに些細な矛盾が含まれてゐたとしても、それが (古典的論理のやうに) 無關係な結論を導くことを許容してはならないといふ考へ方である。この四値論理の具體的な形式は、上述の動機附けとなる考察と、ダナ・スコットが提唱した「近似束」に關する槪念との相互作用から「導出される」ものとなってゐる。
眞理値 : T$ \{\top\}、F$ \{\bot\}、N$ \{\}、B$ \{\top,\bot\}
L4 (論理束 (logical lattice))
論理順序 (眞理順序 (truth order))
$ F\le_L N\le_L T
$ F\le_L B\le_L T
code:mmd
flowchart LR
F --> B --> T
F --> N --> T
結びを$ \land(連言)、交はりを$ \lor(選言) と書く
table:∧
T F N B
T T F N B
F F F F F
N N F N F
B B F F B
table:∨
T F N B
T T T T T
F T F N B
N T N N T
B T B T B
A4 (近似束 (approximation lattice))
情報順序 (information order。knowledge order)
$ N\le_A T\le_A B
$ N\le_A F\le_A B
code:mmd
flowchart BT
N --> F --> B
N --> T --> B
結びを$ \otimes(合意 (consensus))、交はりを$ \oplus(受容 (accept all)) と書く
table:⊗
T F N B
T T N N T
F N F N F
N N N N N
B T F N B
table:⊕
T F N B
T T B T B
F B F F B
N T F N B
B B B B B
$ Bを臺集合として、組$ (B,\land,\lor)と組$ (L,\otimes,\oplus)が共に束 (lattice)であるならば、組$ (B,\land,\lor,\otimes,\oplus)を前雙束と呼ぶ 組$ (B,\land,\lor,\otimes,\oplus)が前雙束であるとして、$ \neg:B\to Bが以下を滿たすならば、組$ (B,\land,\lor,\otimes,\oplus,\neg)を雙束 (bilattice)と呼ぶ 記號
$ (B,\land,\lor)の定める順序を$ \le_Lと書く
$ (L,\otimes,\oplus)の定める順序を$ \le_Aと書く
眞理反轉。$ a\le_L bならば$ \neg b\le_L\neg a
情報保存。$ a\le_A bならば$ \neg a\le_A\neg b
interlaced
$ a\le_L bならば、$ a\otimes c\le_L b\otimes cかつ$ a\oplus c\le_L b\oplus c
$ a\le_A bならば、$ a\land c\le_A b\land cかつ$ a\lor c\le_A b\lor c
分配的 (distributive)
$ a\lor(b\otimes c)=(a\otimes b)\lor(a\otimes c)等
分配的ならば interlaced である
論理行列 (logical matrix)$ M=(V,D,O)
$ D: 指定値 (designated elements)。眞と見做される値の集合
$ O: 演算の解釋。眞理値表
歸結關係$ \Gamma\vdash\psi
$ \Gammaの含む全ての式を指定値$ Dに寫す任意の賦値が、$ \psiもまた$ Dに寫す table:¬
T F N B
F T N B
$ V:=\{T,F,N,B\}
$ D:=\{T,B\}
$ O:$ (\land,\lor,\neg)
分配的
$ {\cal FOUR}={\cal TWO}\odot{\cal TWO}
$ {\cal TWO}:=(\{0,1\},0\le 1)
$ T=(0,1),$ F=(1,0),$ N=(0,0),$ B=(1,1)
$ (\{T,F,N,B,dt,df,m\},\neg)の成す$ \cal SEVEN($ \cal DEFAULT)
$ dt: default true
$ df: default false
$ m: maybe
論理順序
$ F\le_L df
$ dt\le_L T
code:mmd
flowchart LR
F --> B --> T
F --> m --> T
df --> m --> dt
df --> N --> dt
F --> df
dt --> T
情報順序
code:mmd
flowchart BT
N --> df --> F --> B
df --> m --> F
dt --> m --> T
N --> dt --> T --> B
table:¬
T F N B dt df m
F T N B df dt m
interlaced でない
$ \cal NINE
$ pt: 部分的に眞
$ pf: 部分的に僞
論理順序
code:mmd
flowchart LR
F --> pf --> B --> pt --> T
pf --> m --> pt
df --> m --> dt
F --> df --> N --> dt --> T
情報順序
code:mmd
flowchart BT
N --> df --> F --> pf --> B
df --> m --> pf
dt --> m --> pt
N --> dt --> T --> pt --> B
$ {\cal NINE}={\cal THREE}\odot{\cal THREE}
$ {\cal THREE}:=(\{0,\frac 1 2,1\},0\le\frac 1 2\le 1)
$ m=(\frac 1 2,\frac 1 2)
$ dt=(\frac 1 2,0),$ df=(0,\frac 1 2)
$ pt=(1,\frac 1 2),$ pf=(\frac 1 2,1)
積による構成$ {\cal L}\odot{\cal L}
$ {\cal L}=(L,\le)を完備束とする 以下の構成は雙束 (bilattice)$ {\cal L}\odot{\cal L}=(L\times L,\le_L,\le_A,\neg)となる $ (a_1,a_2)\le_L(b_1,b_2)iff.$ a_1\le b_1かつ$ b_2\le a_2
$ (a_1,a_2)\le_A(b_1,b_2)iff.$ a_1\le b_1かつ$ a_2\le b_2
$ \neg(a_1,a_2):=(a_2,a_1)
區閒 (interval) による構成$ {\cal I}({\cal L})
$ {\cal L}=(L,\le)を完備束とする 以下の構成は前雙束$ {\cal I}({\cal L})=(I({\cal L}),\le_L,\le_A)となる $ I({\cal L}):=\{[a,b]|a\le b\}
閉區閒$ [a,b]:=\{c|a\le c\le b\}
$ [a_1,a_2]\le_L[b_1,b_2] iff.$ a_1\le b_1かつ$ a_2\le b_2
$ [a_1,a_2]\le_A[b_1,b_2] iff.$ a_1\le b_1かつ$ b_2\le a_2
區閒の包含
有限多値論理へ擴張できる
論理雙束 (logical bilattice)$ ({\cal B},{\cal F})
$ \cal Fは$ \cal Bの prime bifilter
bifilter$ {\cal F}\subset{\cal B},$ {\cal F}\ne\varnothing
$ a\land b\in{\cal F}iff.$ a\in{\cal F}かつ$ b\in{\cal F}
$ a\otimes b\in{\cal F}iff.$ a\in{\cal F}かつ$ b\in{\cal F}
prime bifilter
$ \cal Fは bifilter である
$ a\lor b\in{\cal F}iff.$ a\in{\cal F}または$ b\in{\cal F}
$ a\oplus b\in{\cal F}iff.$ a\in{\cal F}または$ b\in{\cal F}
本論文では、現在の人工知能硏究における推論システムに關する主要な硏究成果を、統一的な形式體系として定式化する手法を提案する。本硏究では、一階定理證明系、前提ベース眞理維持システム (ATMS。assumption-based truth maintenance systems)、デフォルト論理や周緣化といった未實裝の形式システムなど、多くの既存システムが單一の汎用フレームワークによって包含可能であることを示す。
まずこのフレームワークを定義するが、これは「雙束 (bilattice)」として知られる數學的構造を基盤としてゐる。この構造を用ゐた推論の形式的定義を提示し、この定義が ATMS や特定の單純な非單調論理に關する既存硏究を一般化するものであることを實證する。 理論的な說明に續いて、本硏究ではこの設定における推論に對する構成的アプローチを提示する。その結果、從來の推論手法と ATMS の兩方を一般化した手法を、いかなる實質的な計算オーバーヘッドも發生させることなく實現した。さらに、本手法は default 推論器の實裝にも適用可能であることを示すとともに、default 推論手法と ATMS 手法を組み合はせた新たなアプローチについて論じる。この組み合はせにより、我々は「漸進的」な default 推論システムを形式的に記述することが可能となった。この漸進的システムは、暫定的な結論を導出する前に整合性チェックを行ふ必要がなく、代はりに說得力のある矛盾する證據が提示された場合に、デフォルト前提や結論を適宜修正することができる。このため、本システムは從來のアプローチに比べてはるかに計算效率に優れてゐる。 最後に、我々が提案する多値論理アプローチを實裝する際の具體的な方法について論じる。まず、我々が提案するやうな多値論理アプローチを實裝する際に對處すべき一般的な課題について考察する。その後、既存の實裝結果を示す具體的な事例について檢討する。この單一の實裝は、以下の用途に用ゐられる : 第一階論理を用いたデジタルシミュレーションタスク、de Kleer と Williams が提案した ATMS を用ゐた診斷タスク、Reiter の default 推論や McCarthy の周緣化理論における default 推論問題、そしてデフォルト手法と正當化情報を組み合はせより效率的に同じ問題を解決する場合である。これらすべての應用事例では、同一の汎用雙束 (bilattice)定理證明器が使用されてをり、異なるのは檢討對象となる雙束 (bilattice)の選擇のみである。 ギンスバーグによって提唱された雙束 (bilattice)とは、情報の缺落や矛盾を優雅に扱へる眞理値空閒の一種である。最も單純な例として、古典的な二値論理を基礎とした Belnap の四値論理が擧げられる。その他の具體例としては、有限値多値論理や確率値論理を基盤とするものが存在する。本硏究では、論理プログラミング向けに不動點意味論を構築し、任意の雙束 (bilattice)を眞理値空閒として採用可能とした。數學的枠組みは古典的な二値論理の場合よりも若干複雜になるものの、この成果は信賴度要因を含む分散型論理プログラムに對して自然な意味論を提供するものである。古典的な二値論理とクリプキ＝クリーネの三値論理は、いずれも本硏究で扱ふ論理の自然な部分論理として包含されることになる。これは、本硏究で用ゐる論理がベルナップ論理、すなわち最も單純な雙束 (bilattice)によって定義される論理の自然な部分論理であるためである。 本硏究の目的は、オフェル・アリエリとアルノン・アヴロンが 1990 年代に提唱した雙束 (bilattice)を基盤とする論理體系について、抽象代數的論理學の觀點から體系的な硏究を行ふことである。このやうな硏究を動機づける要因は主に二つある。第一に、雙束 (bilattice)は理論的コンピュータサイエンスや人工知能分野を中心に、ここ 20 年閒で多樣な應用分野を生み出してきた洗練された形式體系としての關心がある。本硏究は、このやうな應用の基盤となる數學的・論理的枠組みの理解を深めることに貢獻することを目指してゐる。第二に、雙束 (bilattice)に基づく論理體系への我々の關心は、抽象代數的論理學に由來する。廣義に言へば、代數的論理學とは代數學と論理學の閒の關係性を硏究する學問分野である。本硏究を推進する主要な動機の一つは、代數的手法を用ゐて論理學的問題を解決し、その逆も可能にする點にある。これは具體的には、論理體系に對してその論理の代數的對應物と見なせる代數的モデルのクラスを對應させることで實現される。タルスキとその共同硏究者らの硏究を出發點として、論理の代數化手法は過去 20 年閒でますます發展・一般化されてきた。特に過去 20 年閒において、代數論理學者たちは論理の代數化プロセスそのものに着目し、この種の硏究は現在では抽象代數的論理學 (AAL と略記) として知られる代數論理學の一分野を形成してゐる。 本論文では、ベルナップの考案した實用的な Belnap の四値論理と技術的あるいは哲學的槪念を共有する理論計算機科學の 4 つの硏究分野について考察する。驚くべきことに、ベルナップ＝ダン論理からの着想が認められてゐるのは、d-フレームの硏究分野においてのみである。ベルナップの硏究と線形論理、Blame Calculus、あるいは LVars の硏究との關聯性については、公然と認められることはない。 これら 3 つの關聯性の核心は、雙束 (bilattice)のツイスト積表現を通じて理解される。一方で、この表現方法により、線形論理の大規模なモデルクラスをベルナップ＝ダン論理を基盤として解釋することが可能となる。他方で、d-フレームには 2 つの異なるツイスト積表現定理が存在し、さらに Blame Calculus の核心的な定理も、嚴密な證明理論的風味を伴ひつつも、本質的にはツイスト積表現定理の一種と見なすことができるのである。 d-frame
本論文では、フレーム理論を基礎として、雙位相空閒に對する Stone 雙對性を導入する。中核となる槪念は「d-フレーム」であり、これは二つの開集合ラティスを公理的に定式化したものである。この槪念から導かれる「d-健全性」の槪念を考察すると、これは從來の健全性槪念よりもはるかに廣範な槪念であることが判明した。空閒的 d-フレームからは、さらなる公理が導出され、これに基づいて「合理的なd-フレーム」を定義することが可能となる。これらのフレームは、部分フレームとして別の表現も可能である。本硏究では、二位相空閒における正規性およびコンパクト性の自然な槪念を探求し、それらがd-フレームにおいてどのやうに現れるかを明らかにする。これにより、この一般的な枠組みの中で、古典的なストーン型雙對性――具對的には Boolean 代數および有界分配ラティスに對する Stone 雙對性、本硏究の著者らが提唱する强近接ラティス (否定演算附き) に對する雙對性、および古典的フレームの雙對性――を正確に位置附けるための理論的枠組みが構築される。この一般雙對性は、一方の位相における開集合を命題論理式の正の範圍として、他方の位相における開集合を負の範圍として解釋することで論理的に解釋可能である。この視點は、特定の狀態においては命題が判定不能となり得ること、また別の狀態においては自己矛盾を生じ得るといふ事實を浮き彫りにする。さらに、我々は命題論理式の集合上に二つの自然な順序關係を導出する。一つはスコットの情報順序と關聯するものであり、もう一つは通常の論理的含意關係である。これら二つの順序關係の相互作用こそが、本硏究の主要な組織原理と言へる。 雙位相空閒 (bitopological space)
雙束 (bilattice)とフレームは、理論計算機科学において廣く應用されてゐる數學的構造であるが、それぞれ全く異なる分野で活用されてゐる。 近年、部分的かつ矛盾する情報を扱へるやうにフレームを一般化した d-フレームが導入されたことで、これら二つの形式體系を統合する道が開かれた。
本提案の目的は、この可能性を探求し、理論的に嚴密かつ汎用性の高い形式體系を構築することにある。これにより、雙束 (bilattice)のアプローチと d-フレームのアプローチを統一的に扱ふことが可能となり、領域理論に對して根本的な影響を與へるとともに、雙束 (bilattice)を基盤とする他の形式體系にも重要な影響を及ぼすことが期待される。 この目的を達成するためには、まず第一に、雙束 (bilattice)硏究において有效性が實證された代數的・論理的手法をd-フレーム理論に適用し、d-フレームを支へる論理體系のより深い理解の構築と確立を圖る。第二に、雙束 (bilattice)の適用範圍を領域理論の枠組みに擴張し、完全性や位相的雙對性といった問題に焦點を當てた硏究を展開する。 具體的には、(1) 雙束 (bilattice)硏究において有效性が實證された代數的・論理的手法をd-フレーム理論に適用し、d-フレームを支へる論理體系のより深い理解の構築と確立を圖ること、ならびに (2) 雙束 (bilattice)の適用範圍を領域理論の枠組みに擴張し、完全性や位相的雙對性といった問題に焦點を當てた硏究を展開することを通じて、この目的を達成する。 Blame Calculus に於ける部分型關係
スクリプトが本格的なアプリケーションへと發展するにつれ、プログラマーはスクリプト言語で記述したプログラムの一部を、堅牢で豊富な型システムを備へた言語へ移植したいと考へるやうになる。このやうな言語閒移行の手法は、型安全性を保證するとともに、他のアプリケーションでの再利用に對しても最小限の保證を提供する。本論文では、この種の言語閒移行を實現するためのフレームワークを提案する。具體的には、型附けされていないラムダ計算で記述されたモジュール群から構成されるプログラムを對象とし、そのうちの 1 つのモジュールを單純型附きラムダ計算で書き換へることで、元のプログラムと同等の機能を保持しつつ、期待されるレベルの型安全性が追加されることを數學的に證明する。すなわち、型附けされたモジュール內のコードは誤動作を起こさないことが保證される。これらの保證を確實にするため、移行プロセスでは靜的に型附けされたモジュールから制約を推論し、それを動的に型附けされたモジュールに對して動作契約の形式で適用する。
LVars (lattice-based variables)
決定性を設計段階から組み込んだ竝列計算モデルを用いて記述されたプログラムは、常に同じ觀測可能な結果を生成することが保證される。これにより、竝列ソフトウェア開發において問題となる、再現が困難な微妙な非決定性バグから解放されるといふ利點がある。本論文では、既存の單一代入モデルを一般化した新たな決定性竝列プログラミングモデル「LVars」を提案する。LVars では、ユーザーが指定した束 (lattice)構造に對して單調増加する複數の代入操作を許可することで、決定性を保證する。具體的には、單調増加する書き込み操作のみを許可するとともに、「閾値」讀み取り操作を導入することで、下限値が滿たされるまで處理を待機させる。本論文では、LVars モデルにおける決定性の證明を提示するとともに、LVars を採用した言語のプロトタイプ實装について說明する。さらに、LVars モデルを擴張し、失敗は許容するが誤った結果は決して生じない、といふ限定的な非決定性をサポートするための手法についても詳述する。